A:Type, B:(AType), eq:EqDecider(A), f,g:fpf(A; a.B(a)), x:A.
(fpf-dom(eq; x; fpf-join(eq; f; g)))
 (fpf-ap(fpf-join(eq; f; g); eq; x)
 (=
 (if fpf-dom(eq; x; f) then fpf-ap(f; eq; x) else fpf-ap(g; eq; x) fi 
 ( B(x)) 

latex

Definitions	x:A. B(x), x(s), P  Q, fpf-join(eq; f; g), fpf-ap(f; eq; x), if b then t else f fi , t.2, fpf-cap(f; eq; x; z), t  T, tt, x. t(x), ff, prop{i:l}, , Unit, P  Q, P  Q, A, P  Q, False,
Lemmas	fpf-dom wf, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-join wf, top wf, fpf-trivial-subtype-top, fpf wf, deq wf, fpf-join-dom